package arlab.formulae.transformations
import arlab.formulae._
import scala.Math._
import actors.threadpool.Executors.FinalizableDelegatedExecutorService
import arlab.picosat2._

object Transformations{

   //Transformation in die NNF
   def nnf(fm: Formula):Formula = fm match {
        case And(a,b) => And(nnf(a),nnf(b))
        case Or(a,b) => Or(nnf(a),nnf(b))
        case ForAll(x,a) => ForAll(x,nnf(a))
        case Exists(x,a) => Exists(x,nnf(a))
        case Not(Not(a)) => nnf(a)
        case Not(True) => False
        case Not(False) => True
        case Not(And(a,b)) => Or(nnf(Not(a)),nnf(Not(b)))
        case Not(Or(a,b)) => And(nnf(Not(a)),nnf(Not(b)))
        case Not(ForAll(x,a)) => Exists(x,nnf(Not(a)))
        case Not(Exists(x,a)) => ForAll(x,nnf(Not(a)))
        case Not(Globally(a)) => Finally(nnf(Not(a)))
        case Not(Finally(a)) => Globally(nnf(Not(a)))
        case Not(Next(a)) => Next(nnf(Not(a)))
        case Not(Until(a,b)) => Release(nnf(Not(a)), nnf(Not(b)))
        case Not(Release(a,b)) => Until(nnf(Not(a)), nnf(Not(b)))
        case other => other   
   }

        
   //Transformation in die CNF
   def cnf(fm: Formula):Formula = nnf(fm) match{
        case Or(a,b) => distrib(Or(cnf(a),cnf(b)))
        case And(a,b) => And(cnf(a),cnf(b))
        case other => nnf(other)   
   }
   
   def distrib(fm: Formula):Formula = fm match{
        case Or(And(a,b),c) => And(distrib(Or(a,c)),distrib(Or(b,c)))
        case Or(a,And(b,c)) => And(distrib(Or(a,b)),distrib(Or(a,c)))
        case other => other
   }
   
   
   def simplify(fm: Formula):Formula = fm match{
        case And (a,True) => simplify(a)
        case And (True,a) => simplify(a)
        case And (a,False) => False
        case And (False,a) => False
        
        case Or (a,True) => True
        case Or (True,a) => True
        case Or (a,False) => simplify(a)
        case Or (False,a) => simplify(a)
        
        case Not(True) => False
        case Not(False) => True
        case Not(Not(a)) => simplify(a)
        case Not(a) => Not(simplify(a))
        
        case And(a,b) if a == b => simplify(a)
        case Or(a,b) if a == b => simplify(a)
        
        case And(Not(a),b) if a == b => False
        case And(a,Not(b)) if a == b => False
        case Or (Not(a),b) if a == b => True
        case Or (a,Not(b)) if a == b => True
        
        case And(a,b) => simplifyNoRecursion(And(simplify(a),simplify(b)))
        case Or(a,b) => simplifyNoRecursion(Or(simplify(a),simplify(b)))
        
        case other => other        
   }
   
   def simplifyNoRecursion(fm: Formula):Formula = fm match{
        case And (a,True) => simplify(a)
        case And (True,a) => simplify(a)
        case And (a,False) => False
        case And (False,a) => False
        case Or (a,True) => True
        case Or (True,a) => True
        case Or (a,False) => simplify(a)
        case Or (False,a) => simplify(a)
        case Not(True) => False
        case Not(False) => True
        case Not(Not(a)) => simplify(a)
        case Not(a) => Not(simplify(a))
        
        case And(a,b) if a == b => simplify(a)
        case Or(a,b) if a == b => simplify(a)
               
        case other => other        
   }
   
   var counter = -1
   //Skolemisiert eine Funktion
   def skolemize(fm: Formula): Formula = nnf(fm) match{
        
        case And(a,b) => And(skolemize(a),skolemize(b))
        case Or(a,b) => Or(skolemize(a),skolemize(b))
        case ForAll(x,a) => ForAll(x,skolemize(a))
        case Exists(x,a) => {
                                counter = counter +1 
                                //skolemize(a)
                                skolemize(a.subst(Map().updated(x, Function("sk" + counter, Exists(x,a).free.toArray:_*))))
                            }
        case other => nnf(fm)
   }
   
   
   def pnf(fm: Formula): Formula = nnf(fm) match{
   
        case ForAll(x,a) => ForAll(x,pnf(a))
        case Exists(x,a) => Exists(x,pnf(a))
        case And(ForAll(x,a),b) => if (b.free(x)) pnf(And(ForAll(x.variant(b.free), a.subst(Map().updated(x,x.variant(b.free)))),b))
                                   else ForAll(x,pnf(And(a,b)))
        case And(a,ForAll(x,b)) => pnf(And(ForAll(x,b),a))
        case Or(ForAll(x,a),b) =>  if (b.free(x)) pnf(Or(ForAll(x.variant(b.free), a.subst(Map().updated(x,x.variant(b.free)))),b))
                                   else ForAll(x,pnf(Or(a,b)))
        case Or(a,ForAll(x,b)) =>pnf(Or(ForAll(x,b),a))
        
        case And(Exists(x,a),b) => if (b.free(x)) pnf(And(Exists(x.variant(b.free), a.subst(Map().updated(x,x.variant(b.free)))),b))
                                   else Exists(x,pnf(And(a,b)))
        case And(a,Exists(x,b)) => pnf(And(Exists(x,b),a))
        case Or(Exists(x,a),b) =>  if (b.free(x)) pnf(Or(Exists(x.variant(b.free), a.subst(Map().updated(x,x.variant(b.free)))),b))
                                   else Exists(x,pnf(Or(a,b)))
        case Or(a,Exists(x,b)) =>pnf(Or(Exists(x,b),a))
        
        
        case And(a,b) => pnfNoRekursion(And(pnf(a),pnf(b)))
        case Or(a,b) => pnfNoRekursion(Or(pnf(a),pnf(b)))
                
        case other => nnf(fm)
   }
   
   def pnfNoRekursion(fm: Formula): Formula = fm match{
   
        case And(ForAll(x,a),b) => if (b.free(x)) pnf(And(ForAll(x.variant(b.free), a.subst(Map().updated(x,x.variant(b.free)))),b))
                                   else ForAll(x,pnf(And(a,b)))
        case And(a,ForAll(x,b)) => pnf(And(ForAll(x,b),a))
        case Or(ForAll(x,a),b) =>  if (b.free(x)) pnf(Or(ForAll(x.variant(b.free), a.subst(Map().updated(x,x.variant(b.free)))),b))
                                   else ForAll(x,pnf(Or(a,b)))
        case Or(a,ForAll(x,b)) =>pnf(Or(ForAll(x,b),a))
        
        case And(Exists(x,a),b) => if (b.free(x)) pnf(And(Exists(x.variant(b.free), a.subst(Map().updated(x,x.variant(b.free)))),b))
                                   else Exists(x,pnf(And(a,b)))
        case And(a,Exists(x,b)) => pnf(And(Exists(x,b),a))
        case Or(Exists(x,a),b) =>  if (b.free(x)) pnf(Or(Exists(x.variant(b.free), a.subst(Map().updated(x,x.variant(b.free)))),b))
                                   else Exists(x,pnf(Or(a,b)))
        case Or(a,Exists(x,b)) =>pnf(Or(Exists(x,b),a))
        
        case ForAll(x,a) => ForAll(x,pnf(a))
        case Exists(x,a) => Exists(x,pnf(a))
                
        case other => fm
   }
  // Methode, die für eine Formel in PNF die Matrix 
  def matrix (fm:Formula) : Formula = pnf(fm) match{
    case ForAll(x,a) => matrix(a)
    case Exists(x,a) => matrix(a)
    case other => fm
    
  }
   
   
   def generalize(fm: Formula): Formula = generalizeHelp(fm, fm.free)
   def generalizeHelp(fm:Formula, free:Set[Variable]):Formula = 
        if (free.isEmpty) fm
        else generalizeHelp(ForAll(free.head, fm),free.tail)


   var tseitinCounter = -1
   
   def tseitincnf2(fm:Formula):Formula = {
        val ts = tseitincnf_helper(simplify(nnf(fm)))
        simplify(nnf(And(ts._1, ts._2)))
   }
   def tseitincnf_helper(fm:Formula):(Formula, Formula) = fm match {
                  
        case BooleanVariable(s) => (BooleanVariable(s), True)
        case Not(a) => (Not(a), True)
          
        case And(a,b) => {
            val a2 = tseitincnf_helper(a)
            val b2 = tseitincnf_helper(b)
            
            tseitinCounter = tseitinCounter + 1
            val ts = BooleanVariable("ts"  + tseitinCounter)
            
            (ts, And(ts.tseit_implic(And(a2._1, b2._1)), 
                               And(a2._2, b2._2)))
        }
        
        case Or(a,b) => {
            val a2 = tseitincnf_helper(a)
            val b2 = tseitincnf_helper(b)
            
            tseitinCounter = tseitinCounter + 1
            val ts = BooleanVariable("ts"  + tseitinCounter)
            
            (ts, And(ts.tseit_implic(Or(a2._1, b2._1)), 
                               And(a2._2, b2._2)))
        }
   }
   /*
   def tseitincnf(fm: Formula): Formula = { 
      nnf(fm) match{
        case Or(And(a,b),c) => {
                                tseitinCounter = tseitinCounter + 1
                                tseitincnf(And(And(Or(c,BooleanVariable("ts" + tseitinCounter)),
                                                   Or(b,Not(BooleanVariable("ts" + tseitinCounter)))),
                                               Or(a,Not(BooleanVariable("ts" + tseitinCounter)))))
                               }
        case Or(a,And(b,c)) => tseitincnf(Or(And(b,c),a))
        
        case And(a,b) => And(tseitincnf(a),tseitincnf(b))
        
        case Or(Or(a,b),c) => tseitincnf(Or(c,Or(a,b)))
        case Or(a,Or(b,c)) => tseitinNoRekursion(Or(tseitincnf(a), tseitincnf(Or(b,c))))
        
        case other => fm        
      }
   }
   
   def tseitinNoRekursion(fm: Formula): Formula = fm match{
        case Or(And(a,b),c) => {
                                tseitinCounter = tseitinCounter + 1
                                tseitincnf(And(And(Or(c,BooleanVariable("ts" + tseitinCounter)),
                                                   Or(b,Not(BooleanVariable("ts" + tseitinCounter)))),
                                               Or(a,Not(BooleanVariable("ts" + tseitinCounter)))))
                               }
        case Or(a,And(b,c)) => tseitincnf(Or(And(b,c),a))
        case And(a,b) => And(tseitincnf(a),tseitincnf(b))
        
        case Or(Or(a,b),c) => tseitincnf(Or(c,Or(a,b)))        
        case other => fm        
   }
   */
   
   def LTL_To_Boolean_Loop(fm:Formula, i:Int, l:Int, k:Int):Formula = simplify(nnf(fm)) match{
        case BooleanVariable(string) => BooleanVariable(string + i)
        case Not(BooleanVariable(string)) => Not(BooleanVariable(string + i))

        case And(a,b) => And(LTL_To_Boolean_Loop (a, i, l, k), LTL_To_Boolean_Loop (b, i, l, k))
        case Or(a,b) => And(LTL_To_Boolean_Loop (a, i, l, k), LTL_To_Boolean_Loop (b, i, l, k))
        
        case Globally(a) => AND({(i2:Int, k2:Int) => LTL_To_Boolean_Loop(a,i2, l, k2)}, min(i,l), k)
       
        case Finally(a) =>  OR({(i2:Int, k2:Int) => LTL_To_Boolean_Loop(a,i2, l, k2)}, min(i,l), k)
       
        case Next(a) => LTL_To_Boolean_Loop(a, i+1, l,k)
        case Until(a,b) => Or(OR({(j:Int, k2:Int) => 
                                 And(LTL_To_Boolean_Loop(b, j, l, k2), 
                                     AND({(n:Int, k2:Int) =>LTL_To_Boolean_Loop(a, n, l, k2)}, i , j-1))},k,i),
                              OR({(j:Int, k2:Int) => And(LTL_To_Boolean_Loop(b, j, l, k2), 
                                                         And(AND({(n:Int, k2:Int) => LTL_To_Boolean_Loop(a, n, l, k2)},i,k),
                                                             AND({(n:Int, k2:Int) => LTL_To_Boolean_Loop(a, n, l, k2)}, l, j-1)))}, l, i-1))

        case Release(a,b) => Or(AND({(j:Int, k2:Int) => LTL_To_Boolean_Loop(b, j, l, k)},min(i,l), k),
                               Or(OR({(j:Int,  k2:Int) => And(LTL_To_Boolean_Loop(a, j, l, k), 
                                                              AND({(n:Int, k2:Int)=> LTL_To_Boolean_Loop(b, n, l, k)}, i,j))}, i,k),

                                 OR({(j:Int, k2:Int) => And(LTL_To_Boolean_Loop(a, j, l, k2),
                                   And(AND({(n:Int, k2:Int) => LTL_To_Boolean_Loop(b, n, l, k2)},i,k),
                                     AND({(n:Int, k2:Int) => LTL_To_Boolean_Loop(b, n, l, k2)}, l, j)))}, l, i-1)))
        
        
        case other => fm
   
   }
   
   def LTL_To_Boolean_No_Loop(fm:Formula, i:Int, k:Int):Formula = simplify(nnf(fm)) match{
        case BooleanVariable(string) => BooleanVariable(string + i)
        case Not(BooleanVariable(string)) => Not(BooleanVariable(string + i))
        
        case And(a,b) => And(LTL_To_Boolean_No_Loop (a, i, k),LTL_To_Boolean_No_Loop (b, i, k))
        case Or(a,b) => And(LTL_To_Boolean_No_Loop(a, i, k), LTL_To_Boolean_No_Loop (b, i, k))
        case Globally(a) => False
        case Finally(a) => OR({(j:Int, k2:Int) => LTL_To_Boolean_No_Loop(a,j,k2)} ,i,k)
        case Next(a) => if (i < k) LTL_To_Boolean_No_Loop(a, i+1, k)
                        else False
        case Until(f,g) => OR({(j:Int, k2:Int) => 
                                 And(LTL_To_Boolean_No_Loop(g, j, k2), 
                                     AND({(n:Int, k3:Int) =>LTL_To_Boolean_No_Loop(f, n, k3)}, i , j-1))},k,i)
                                     
        case Release(f,g) => OR({(j:Int, k2:Int) => 
                                 And(LTL_To_Boolean_No_Loop(f, j, k2), 
                                     AND({(n:Int, k3:Int) =>LTL_To_Boolean_No_Loop(g, n, k3)}, i , j))},k,i)
        
   }
   
   
   
   def LoopCondition(k:Int, kripke: Kripke): Formula = {
        OR({(i:Int, k2: Int) => kripke.step(k2,i)}, 0,k)
   }
   def generateTranslation(kripke: Kripke, ltl: Formula, k: Int):Formula = {
    //   println("generate Translations")   
   
       And( And(kripke.init(0), AND({(i:Int, k2: Int) => kripke.step(i, i+1)}, 0, k-1)),
            Or(And(Not(LoopCondition(k, kripke)),LTL_To_Boolean_No_Loop(ltl, 0, k)),
               OR({(l:Int, k2: Int) => And(kripke.step(k,l), LTL_To_Boolean_Loop(ltl, 0, l, k))}, 0, k)))
   }
   
   //liefert eine formel in cnf
   def boundModelLTL(kripke: Kripke, ltl: Formula, k: Int) = {
        val s = sat
        s.picosat_init()
    //    println(generateTranslation(kripke, ltl, k))
    //    println()
    //    println(tseitincnf2(generateTranslation(kripke, ltl, k)))
        val ret = s.solve(simplify(nnf(tseitincnf2(generateTranslation(kripke, ltl, k)))))
              
        s.picosat_reset()
        ret   
   }
   
   def AND (fm:(Int,Int) => Formula, i:Int, k:Int):Formula = if (i == k) fm(i,k)
                                                           else And(fm(i,k), AND(fm, i+1, k))
                                                           
   def OR (fm:(Int,Int) => Formula, i:Int, k:Int):Formula = if (i == k) fm(i,k)
                                                           else Or(fm(i,k), OR(fm, i+1, k))

}


